In this paper we consider the problem of building rich categories of setoids,in standard intensional Martin-L\"of type theory (MLTT), and in particular howto handle the problem of equality on objects in this context. Any(proof-irrelevant) family F of setoids over a setoid A gives rise to a categoryC(A, F) of setoids with objects A. We may regard the family F as a setoid ofsetoids, and a crucial issue in this article is to construct rich or largeenough such families. Depending on closure conditions of F, the category C(A,F) has corresponding categorical constructions. We exemplify this with finitelimits. A very large family F may be obtained from Aczel's model constructionof CZF in type theory. It is proved that the category so obtained is isomorphicto the internal category of sets in this model. Set theory can thus establish(categorical) properties of C(A, F) which may be used in type theory. We alsoshow that Aczel's model construction may be extended to include the elements ofany setoid as atoms or urelements. As a byproduct we obtain a natural extensionof CZF, adding atoms. This extension, CZFU, is validated by the extended model.The main theorems of the paper have been checked in the proof assistant Coqwhich is based on MLTT. A possible application of this development is tointegrate set-theoretic and type-theoretic reasoning in proof assistants.
展开▼
